LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
LeanPRM：基于 Lean 的自然语言证明过程监督
🧭 过程监督 · Lean 自动标注
University of Texas at Austin · University of California, Los Angeles · New York University
利用 Lean 形式化证明自动生成自然语言证明的逐步正确性标签，训练过程监督验证器，步级准确率从 48.2 提升至 74.7
📌 工作参考价值（4 点）
- 对 Agent/多步决策轨迹，可借鉴「可执行环境自动打标签」：用沙盒、规则引擎或领域知识库对中间步骤做形式化校验，替代人工标注，低成本构建过程监督数据。
- 「分离形式错误与语义错误」的过滤模型思路值得迁移：先自动生成大量轨迹标签，再训练一个二分类器剔除仅因语法/格式失败但推理正确的负样本，避免污染奖励模型。
- 训练过程奖励模型时，可以混合少量人工标注与大量自动标注；本工作证明在没有人类标注的情况下，自动标签也能显著优于 PRM800K 人工标注，适合快速迭代线上推理链路。
- 对于电商推荐理由生成、搜索 query 改写等有可执行校验（如转化、点击、库存）的场景，可尝试用业务指标为中间步骤提供弱监督，再微调 LLM 做步骤级打分。